es:ES, a:Atom1, e:E, i:Id. e sends to i || a    

latex

Definitions	x. t(x), P  Q, e sends to i || a , , t  T, x:A. B(x), x(s)
Lemmas	event system wf, es-loc wf, Id wf, es-val wf, es-valtype wf, free-from-atom wf1, es-sender wf, es-E wf, es-isrcv wf, assert wf, alle-at wf